We consider the problem of verifying deadlock freedom for symmetric cachecoherence protocols. In particular, we focus on a specific form of deadlockwhich is useful for the cache coherence protocol domain and consistent with theinternal definition of deadlock in the Murphi model checker: we refer to thisdeadlock as a system- wide deadlock (s-deadlock). In s-deadlock, the entiresystem gets blocked and is unable to make any transition. Cache coherenceprotocols consist of N symmetric cache agents, where N is an unboundedparameter; thus the verification of s-deadlock freedom is naturally aparameterized verification problem. Parametrized verification techniques workby using sound abstractions to reduce the unbounded model to a bounded model.Efficient abstractions which work well for industrial scale protocols typicallybound the model by replacing the state of most of the agents by an abstractenvironment, while keeping just one or two agents as is. However, leveragingsuch efficient abstractions becomes a challenge for s-deadlock: a violation ofs-deadlock is a state in which the transitions of all of the unbounded numberof agents cannot occur and so a simple abstraction like the one above will notpreserve this violation. In this work we address this challenge by presenting atechnique which leverages high-level information about the protocols, in theform of message sequence dia- grams referred to as flows, for constructinginvariants that are collectively stronger than s-deadlock. Efficientabstractions can be constructed to verify these invariants. We successfullyverify the German and Flash protocols using our technique.
展开▼
